Nuprl Lemma : f2f+SDcdr_wf 11,40
es:ES, ff:FIFO, f2f+:F2F+-decls. S_dcdr  i,j:ff.Ce:EDec(ff.S(i,j,e)) 
latex

DefinitionsES, t  T, x:A. B(x), FIFO, F2F+-decls, S_dcdr, x:A  B(x), x:AB(x), ff.C, E, ff.S, f(a), Dec(P)
LemmasF2F+-decls wf, FIFO wf, event system wf

origin